Nuprl Lemma : gen_hyp_tp
13,42
postcript
pdf
A
:Type{i},
e
:
A
,
H
:(
A
Type{j}),
z
:
H
(
e
).
z
0
latex
Up
core
2
,
core
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
origin